g:IMonoid, e:|g|. (1  e) = e 

latex

Up	groups 1
Definitions of Statement	IMonoid
Definitions	t  T, x:A. B(x), P  Q, P & Q, , P  Q, P  Q, False, A, A  B, , True, T, , x f y, IMonoid
Lemmas	imon wf, grp car wf, mon nat op unroll, mon nat op zero, le wf, nat wf, true wf, squash wf, mon nat op wf, grp op wf, mon ident